MsgA
== ds:x:Id fp Type
==  (da:a:Knd fp Type
==  init:x:Id fp ds(x)?Void
==  pre:a:Id fp State(ds)
==  ef:kx::Knd  Id fp State(ds)Valtype(da;kx.1)ds(kx.2)?Void
==  send:kl::Knd  IdLnk fp
==  send:(tg:Id  (State(ds)Valtype(da;kl.1)(da(rcv(kl.2,tg))?Void List))) List
==  frame:x:Id fp Knd List
==  sframe:ltg::IdLnk  Id fp Knd List
==  aframe:k:Knd fp Id List
==  bframe:k:Knd fp IdLnk List
==  rframe:x:Id fp Knd List
==  (prob:a:Id fp FinProbSpace
==  Top)) 

latex

---

clarification:

msga{i:l}
== ds:x:Id fp Type{i}
==  (da:a:Knd fp Type{i}
==  init:x:Id fp fpf-cap(ds;IdDeq;x;Void)
==  pre:a:Id fp State(ds)
==  ef:kx::Knd  Id fp State(ds)Valtype(da;kx.1)fpf-cap(ds;IdDeq;kx.2;Void)
==  send:kl::Knd  IdLnk fp
==  send:(tg:Id  (State(ds)Valtype(da;kl.1)(fpf-cap(da;KindDeq;rcv(kl.2,tg);Void) List))) List
==  frame:x:Id fp Knd List
==  sframe:ltg::IdLnk  Id fp Knd List
==  aframe:k:Knd fp Id List
==  bframe:k:Knd fp IdLnk List
==  rframe:x:Id fp Knd List
==  (prob:a:Id fp FinProbSpace
==  Top)) 

latex

Definitions	Type, , , IdDeq, State(ds), x:AB(x), Valtype(da;k), t.1, f(x)?z, KindDeq, rcv(l,tg), t.2, Void, IdLnk, type List, Knd, x:A  B(x), a:A fp B(a), Id, FinProbSpace, Top
FDL editor aliases	msga